$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, ${\it eq}$:EqDecider($T$), $d$:$a$:$T$ fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. atom{-}free{-}decl\{i:l\}($T$; ${\it eq}$; $d$) $\in$ Prop$_{\mbox{\scriptsize i'}}$